// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_MATH_EXPNAT_MULADD
#define _sHT_MATH_EXPNAT_MULADD

#include <stdint.h>
#include <sHT/math/expnat.h>

// Reverse Proof:
// - a * x + b < expnat(a, e + 1) (and_intros)
// - a * x + b < a * expnat(a, e) (peel expnat)
// - b < a * expnat(a, e) - a * x (omega)
// - b < a * (expnat(a, e) - x) (reverse_distributivity)
// - b < a /\ 0 < a /\ 0 < expnat(a, e) - x (split_mult_order)
// - 0 < expnat(b, e) - x (intuition)
// - x < expnat(b, e) (omega)
// - (assumption)
// Qed.
/*@ lemma expnat_muladd_lt: ∀ ℤ a, x, b, e;
      0 < a && 0 ≤ e && x < expnat(a, e) && b < a
      ==> a * x + b < expnat(a, e + 1); */

#endif
